\begin{tabbing}
$\forall$$A$, $B$:Knd, ${\it es}$:ES, $T$:Type, $m$:$T$.
\\[0ex]$\neg$$A$ $=$ $B$
\\[0ex]$\Rightarrow$ es{-}decls(${\it es}$;"i";;rcv(lnk1\{i to j\},"tg") : $T$)
\\[0ex]$\Rightarrow$ \=@"i"[[[eclor(eclbase($A$;$\lambda$$s$,$v$. true$_{2}$).1;eclthrow(eclbase($B$;$\lambda$$s$,$v$.\+
\\[0ex]true$_{2}$);1))]$\ast$;$A$ sends on lnk1\{i to j\} with tag "tg" [$s$,$v$.$m$], at marker 1;]]
\-\\[0ex]$\Rightarrow$ \=es{-}sends{-}iff2(${\it es}$;lnk1\{i to j\};"tg";$T$;;$e$.kind($e$) $=$ $A$\+
\\[0ex]\& $\forall$$e$$\in$[es{-}init(${\it es}$;$e$),$e$].$\neg$kind($e$) $=$ $B$;$e$.$m$)
\-
\end{tabbing}